It is important to enable reasoning about the meaning and possible effects ofupdates to ensure that the updated system operates correctly. A formal,mathematical model of dynamic update should be developed, in order tounderstand by both users and implementors of update technology what designchoices can be considered. In this paper, we define a formal calculus$update\pi$, a variant extension of higher-order $\pi$ calculus, to modeldynamic updates of component-based software, which is language and technologyindependent. The calculus focuses on following main concepts: propergranularity of update, timing of dynamic update, state transformation betweenversions, update failure check and recovery. We describe a series of rule onsafe component updates to model some general processes of dynamic update anddiscuss its reduction semantics coincides with a labelled transition systemsemantics that illustrate the expressive power of these calculi.
展开▼
机译：重要的是要对更新的含义和可能的影响进行推理，以确保更新的系统正确运行。应该开发一个正式的数学模型来动态更新，以便用户和更新技术的实施者都可以理解可以考虑哪些设计选择。在本文中，我们定义了一种形式的演算$ update \ pi $，它是高阶$ \ pi $演算的变体，用于对基于组件的软件的动态更新进行建模，该更新与语言和技术无关。演算重点关注以下主要概念：更新的粒度，动态更新的时间，版本之间的状态转换，更新失败检查和恢复。我们描述了一系列有关安全组件更新的规则，以对动态更新的一些一般过程进行建模，并讨论其简化语义与表示这些演算表达能力的标记过渡系统语义相吻合。
展开▼
